¬□⊥ → ¬□¬□⊥
第2不完全性定理の内容，すなわち無矛盾(¬□⊥)ならば無矛盾性の証明は不可能(¬□¬□⊥)を形式的に表している． Prop
より強い事実も示しておく．
$ \vdash_\mathsf{GL} \lnot\Box\bot \leftrightarrow \lnot\Box\lnot\Box\bot
proof:
$ \to
1. $ \vdash_\mathsf{K} \bot \to (\Box\bot \to \bot)
2. $ \vdash_\mathsf{K} \bot \to \lnot\Box\bot（$ \lnotdef）
3. $ \vdash_\mathsf{K} \Box \bot \to \Box\lnot\Box\bot（Nec）
4. $ \vdash_\mathsf{K} \lnot\Box\bot \to \lnot\Box\lnot\Box\bot
5. $ \vdash_\mathsf{GL} \lnot\Box\bot \to \lnot\Box\lnot\Box\bot（$ \vdash_\mathsf{K} \varphi \implies \vdash_\mathsf{GL} \varphi）
$ \leftarrow
1. $ \vdash_\mathsf{K} \lnot\Box\bot \to \lnot\Box\bot
2. $ \vdash_\mathsf{K} \lnot\Box\bot \to (\Box \bot \to \bot)
3. $ \vdash_\mathsf{K} \Box\lnot\Box\bot \to \Box(\Box \bot \to \bot)（Nec）
4. $ \vdash_\mathsf{GL} \Box\lnot\Box\bot \to \Box \bot（公理$ \mathsf{L}）
5. $ \vdash_\mathsf{GL} \lnot\Box\lnot\Box\bot \to \lnot\Box\bot
纏めて$ \vdash_\mathsf{GL} \lnot\Box\bot \leftrightarrow \lnot\Box\lnot\Box\bot